Nuprl Lemma : fpf-compose_wf
11,40
postcript
pdf
A
:Type,
B
,
C
:(
A
Type),
f
:
a
:
A
fp
B
(
a
),
g
:(
a
:
A
.
B
(
a
)
C
(
a
)).
g
o
f
a
:
A
fp
C
(
a
)
latex
Definitions
x
:
A
.
B
(
x
)
,
a
:
A
fp
B
(
a
)
,
x
(
s
)
,
t
T
,
g
o
f
,
t
.1
,
t
.2
,
x
.
t
(
x
)
,
f
o
g
,
Lemmas
l
member
wf
,
fpf
wf
origin
A:Type, B, C:(A
Type), f:a:A fp B(a), g:(
a:A.B(a)C(a)). g o f 
a:A fp C(a) A:Type, B, C:(AType), f:a:A fp B(a), g:(a:A.B(a)C(a)). g o f a:A fp C(a) x:A. B(x) B(a) T
x. t(x)